The purpose of a computer program verification system is to analyze a given computer program to determine whether or not it has certain desirable properties. Verification systems can also be used to analyze hardware components, formulae, algorithms, or, more generally, behavioral designs.
A typical verification system works by generating a verification condition (VC) from a given behavioral design, and then processing the verification condition with a theorem prover. A verification condition is a logical formula that, ideally, is valid if and only if all possible behaviors of the design have the desirable properties under consideration. In practice, the verification condition generated may be only an approximation of the ideal verification condition.
The theorem prover should have the property that when it fails to generate a proof, it generates a number of potential counter-examples. The verification system then post-processes these counter-examples into warnings that the desirable properties may not hold. A warning may be spurious; that is, it may warn about something that is not a real error. Spurious warnings may arise when the theorem prover does not have enough information to generate a proof, when the prover is too weak a prover to automatically generate a proof, or when the verification condition produced is not quite the ideal one.
A good verification system has the property that the warnings it produces are informative and easy for a designer to understand. If a warning message is informative and easy to understand, the designer can more easily determine whether a warning is real or spurious, and what its cause is. The designer can then act accordingly, correcting the design at the source of the problem, or ignoring the warning, possibly annotating the design so that the warning will be suppressed next time the verification system is run.
An informative warning message should, ideally, include a characterization of the possible defect (e.g., “array index of out bounds”, “timing constraint not satisfied”, “race condition”, “deadlock”, “failure to establish invariant”) and a source location in the behavioral design where the verification system tried, but failed, to show the absence of the defect (e.g., “line 218 of file ‘ABC.source’”). However, because behavioral designs can include many behaviors that lead to a given source location, a warning message would be even more informative if it provided the sequence or set of behavioral aspects or steps that occur in the scenario of the reported defect, i.e., a program trace. Such behavioral aspects or steps are akin to an execution trace.
There is a class of authoring tools that performs verification functions and generates execution traces. These tools are called dynamic or run-time checkers, because they execute or simulate the execution of the behavioral design in question (i.e., the computer program) and output the active path at the time a possible defect is detected. Examples of such tools are PREfix (Intrinsa Corp., (1998)), which symbolically executes the given program, Testbed Studio, which uses an underlying model checker to perform an exhaustive, back-tracking symbolic simulation of a representation of a given design, and Eraser (Savage, S., et al., “Eraser: A Dynamic Data Race Detector for Multi-threaded Programs”, ACM Transactions on Computer Systems (TOCS), 15(4):391–411, November 1997. Also appeared in Proceedings of the Sixteenth ACM Symposium on Operating System Principles, Oct. 5–8, 1997, St. Malo, France, Operating System Review 31(5), ACM Press, 1997, ISBN 0-89791-916-5, pp 27–37.), which works as the program is actually being executed. In general, run-time checkers entail a number of disadvantages: there may be an overhead to their use, i.e., the program to be checked may be very intensive of resources; some errors in the program may only manifest themselves under certain run-time conditions, such as certain values of the initial parameters; and some errors may be non-reproducible.
By contrast, the present invention falls within a class of program verifiers known as static checkers. Static checkers catch errors at compile time without simulating or executing the program. A research project based on this strategy, the Extended Static Checker (ESC) has been implemented using the technology of program verification. With the ESC, as with static checkers generally, the behavioral design has been annotated by a developer so that the verification condition contains entries associated with specific positions in the source code of the program. The ESC represents a compromise between the rigorous demands of complete program verification and the limited utility of traditional static checkers. Use of a static checker can be important because the cost of a programming error can be greatly reduced if it is detected early in the development process.
Whereas hitherto, static checkers have been successful in pointing out specific source locations where errors or potential errors arise, their applicability has been limited in part because the designer must still ascertain the path that the program took to the error. Accordingly, it is an object of the present invention to cause a static checker to produce program traces that illustrate the possible run-time conditions (e.g., variable values and program execution path) that give rise to the error.